Nuprl Lemma : ma-single-init-feasible
0,22
postcript
pdf
x
:Id,
t
:Type,
v
:
t
. AtomFree(Type;
t
)
Feasible(
x
:
t
initially
x
=
v
)
latex
Definitions
t
T
,
Y
,
false
,
reduce(
f
;
k
;
as
)
,
deq-member(
eq
;
x
;
L
)
,
if
b
t
else
f
fi
,
f
(
x
)
,
x
dom(
f
)
,
b
,
ma-frame-compat(
A
;
B
)
,
f
(
x
)?
z
,
2of(
t
)
,
,
x
:
v
,
mk-ma
,
1of(
t
)
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
P
&
Q
,
x
:
t
initially
x
=
v
,
Feasible(
M
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
False
,
Prop
Lemmas
atom-free
wf
,
IdLnk
wf
,
Knd
wf
,
false
wf
,
bfalse
wf
,
id-deq
wf
,
Id
wf
,
eqof
wf
,
bor
wf
,
assert
wf
origin
x:Id, t:Type, v:t. AtomFree(Type;t) 
Feasible(x : t initially x = v) x:Id, t:Type, v:t. AtomFree(Type;t) Feasible(x : t initially x = v) 
T
t else f fi dom(f)
bxdom(f). v=f(x) P(x;v) Qx:A. B(x)